Nuprl Definition : surject
13,42
postcript
pdf
Surj(
A
;
B
;
f
) ==
b
:
B
.
a
:
A
. (
f
(
a
) =
b
)
latex
clarification:
Surj(
A
;
B
;
f
) ==
b
:
B
.
a
:
A
. (
f
(
a
) =
b
B
)
latex
Up
fun
1
,
fun
1
Wellformedness Lemmas
surject
wf
,
surject
wf
Definitions
x
:
A
.
B
(
x
)
,
x
:
A
.
B
(
x
)
,
s
=
t
,
f
(
a
)
FDL editor aliases
surject
origin
b:B. 
a:A. (f(a) = b)
b:B. a:A. (f(a) = b 
B) b:B. a:A. (f(a) = b)
b:B. a:A. (f(a) = b B) x:A. B(x)x:A. B(x)